\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $L$:($T$ List).\+
\\[0ex](0 $<$ $\parallel$$L$$\parallel$) $\Rightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ ($\neg$($x$ = hd($L$))) $\Rightarrow$ hd($L$) before $x$ $\in$ $L$)
\-
\end{tabbing}